| 1: | fact(X) | → if(zero(X),n__s(0),n__prod(X,fact(p(X)))) | |
| 2: | add(0,X) | → X | |
| 3: | add(s(X),Y) | → s(add(X,Y)) | |
| 4: | prod(0,X) | → 0 | |
| 5: | prod(s(X),Y) | → add(Y,prod(X,Y)) | |
| 6: | if(true,X,Y) | → activate(X) | |
| 7: | if(false,X,Y) | → activate(Y) | |
| 8: | zero(0) | → true | |
| 9: | zero(s(X)) | → false | |
| 10: | p(s(X)) | → X | |
| 11: | s(X) | → n__s(X) | |
| 12: | prod(X1,X2) | → n__prod(X1,X2) | |
| 13: | activate(n__s(X)) | → s(X) | |
| 14: | activate(n__prod(X1,X2)) | → prod(X1,X2) | |
| 15: | activate(X) | → X | |
| 16: | FACT(X) | → IF(zero(X),n__s(0),n__prod(X,fact(p(X)))) | |
| 17: | FACT(X) | → ZERO(X) | |
| 18: | FACT(X) | → FACT(p(X)) | |
| 19: | FACT(X) | → P(X) | |
| 20: | ADD(s(X),Y) | → S(add(X,Y)) | |
| 21: | ADD(s(X),Y) | → ADD(X,Y) | |
| 22: | PROD(s(X),Y) | → ADD(Y,prod(X,Y)) | |
| 23: | PROD(s(X),Y) | → PROD(X,Y) | |
| 24: | IF(true,X,Y) | → ACTIVATE(X) | |
| 25: | IF(false,X,Y) | → ACTIVATE(Y) | |
| 26: | ACTIVATE(n__s(X)) | → S(X) | |
| 27: | ACTIVATE(n__prod(X1,X2)) | → PROD(X1,X2) | |